Nuprl Definition : d-comp-partial-world
0,22
postcript
pdf
d-comp-partial-world(
D
;
v
;
sched
;
dec
;
t
)
== d-partial-world(
D
;CV(d-comp(
D
;
v
;
sched
;
dec
));
t
;
i
.if
t
=
0
x
.M(
i
).init(
x
)?
v
(
i
,
x
)
== d-partial-world(
D
;CV(d-comp(
D
;
v
;
sched
;
dec
));
t
;
i
.
else 1of(CV(d-comp(
D
;
v
;
sched
;
dec
))
== d-partial-world(
D
;CV(d-comp(
D
;
v
;
sched
;
dec
));
t
;
i
.else 1of(
(
t
-1
== d-partial-world(
D
;CV(d-comp(
D
;
v
;
sched
;
dec
));
t
;
i
.else 1of(
,
i
)) fi)
latex
clarification:
d-comp-partial-world(
D
;
v
;
sched
;
dec
;
t
)
== d-partial-world(
D
;CV(d-comp(
D
;
v
;
sched
;
dec
));
t
;
i
.if
t
=
0
x
.d-m(
D
;
i
).init(
x
)?
v
(
i
,
x
)
== d-partial-world(
D
;CV(d-comp(
D
;
v
;
sched
;
dec
));
t
;
i
.
else 1of(CV(d-comp(
D
;
v
;
sched
;
dec
))
== d-partial-world(
D
;CV(d-comp(
D
;
v
;
sched
;
dec
));
t
;
i
.else 1of(
(
t
-1
== d-partial-world(
D
;CV(d-comp(
D
;
v
;
sched
;
dec
));
t
;
i
.else 1of(
,
i
)) fi)
latex
Definitions
d-partial-world(
D
;
f
;
t'
;
s
)
,
if
b
t
else
f
fi
,
i
=
j
,
x
.
A
(
x
)
,
M
.init(
x
)?
v
,
M(
i
)
,
1of(
t
)
,
f
(
a
)
,
CV(
F
)
,
d-comp(
D
;
v
;
sched
;
dec
)
,
n
-
m
,
#$n
FDL editor aliases
d-comp-partial-world
origin